A:Type, eq:EqDecider(A), f:a:A fp Top, x:A. (x  dom(f))  (x  f.1) 

latex

Definitions	t  T, x:A. B(x), EqDecider(T), Top, (x  l), x. t(x), t.1, P  Q, P  Q, P & Q, P  Q, deq-member(eq;x;L), b, , x  dom(f), a:A fp B(a)
Lemmas	all functionality wrt iff, iff functionality wrt iff, assert-deq-member, iff wf, assert wf, deq-member wf, pi1 wf, l member wf, top wf, deq wf